package domains;

import java.math.BigInteger;
import java.util.Arrays;
import java.util.HashMap;
import java.util.Map;
import java.util.Set;

import config.GlobalConfig;
import controlFlowGraph.BinaryOp;
import controlFlowGraph.CFG;
import controlFlowGraph.CFGEdge;
import controlFlowGraph.CFGLabel;
import controlFlowGraph.CFGNode;
import controlFlowGraph.Constant;
import controlFlowGraph.Expression;
import controlFlowGraph.LabAssign;
import controlFlowGraph.LabNop;
import controlFlowGraph.LabPos;
import controlFlowGraph.LabLoad;
import controlFlowGraph.LabNeg;
import controlFlowGraph.LabStore;
import controlFlowGraph.Variable;

public class IntervalAnalysis extends Analysis {

	@Override
	public AnalysisDomain getBottom() {
		return new Bottom();
	}

	@Override
	public AnalysisDomain getTop() {
		Map<Variable, Interval> info = new HashMap<Variable, Interval>();
		for (Variable v : GlobalConfig.variableSet) {
			info.put(v, new Interval(
					new IntervalBound(null, true, false),
					new IntervalBound(null, false, true)));
		}
		return new IntervalDomain(info);
	}

	@Override
	public AnalysisDomain join(AnalysisDomain left, AnalysisDomain right) {
		if(left instanceof Bottom){
			return right;
		}
		if(right instanceof Bottom){
			return left;
		}
		IntervalDomain l = (IntervalDomain) left;
		IntervalDomain r = (IntervalDomain) right;
		Map<Variable,Interval> after_join = new HashMap<Variable,Interval>();
		for(Variable v:GlobalConfig.variableSet){
			Interval new_int = l.getIntervals().get(v).join(r.getIntervals().get(v));
			after_join.put(v, new_int);
		}
		return new IntervalDomain(after_join);
	}

	@Override
	public AnalysisDomain meet(AnalysisDomain left, AnalysisDomain right) {
		if((left instanceof Bottom) || (right instanceof Bottom)){
			return new Bottom();
		}
		IntervalDomain l = (IntervalDomain) left;
		IntervalDomain r = (IntervalDomain) right;
		Map<Variable,Interval> after_meet = new HashMap<Variable,Interval>();
		for(Variable v:GlobalConfig.variableSet){
			Interval new_int = l.getIntervals().get(v).meet(r.getIntervals().get(v));
			// Illegal meet, intervals disjoint, then bottom is a viable choice
			if (new_int == null) {
				return new Bottom();
			}
			after_meet.put(v,new_int);
		}
		return new IntervalDomain(after_meet);
	}

	@Override
	public AnalysisDomain widening(AnalysisDomain left, AnalysisDomain right) {
		if(left instanceof Bottom){
			return right;
		}
		if(right instanceof Bottom){
			return left;
		}
		IntervalDomain l = (IntervalDomain) left;
		IntervalDomain r = (IntervalDomain) right;
		Map<Variable,Interval> after_widening = new HashMap<Variable,Interval>();
		for(Variable v:GlobalConfig.variableSet){
			Interval new_int = l.getIntervals().get(v).widening(r.getIntervals().get(v));
			after_widening.put(v, new_int);
		}
		return new IntervalDomain(after_widening);
	}

	@Override
	public AnalysisDomain narrowing(AnalysisDomain left, AnalysisDomain right) {
		if((left instanceof Bottom) || (right instanceof Bottom)){
			return new Bottom();
		}
		IntervalDomain l = (IntervalDomain) left;
		IntervalDomain r = (IntervalDomain) right;
		Map<Variable,Interval> after_narrowing = new HashMap<Variable,Interval>();
		for(Variable v:GlobalConfig.variableSet){
			Interval new_int = l.getIntervals().get(v).narrowing(r.getIntervals().get(v));
			after_narrowing.put(v,new_int);
		}
		return new IntervalDomain(after_narrowing);
	}

	@Override
	public String printNode(CFGNode node) {
		String res = "";
		if (node.getId() == 0 || node.getId() == -1) {
			if (node.getId() == 0) {
				res += "START : ";
			} else {
				res += "END : ";
			}
		} else {
			res = "P" + node.getId() + " : ";
		}
		AnalysisDomain anaInfo = node.getAnalysisInfo();
		if (anaInfo instanceof Bottom) {
			res += "BOT";
			return res;
		} else {
			res += "{";
		}
		
		IntervalDomain intervalInfo = (IntervalDomain) anaInfo;
		Set<Variable> set = intervalInfo.getIntervals().keySet();
		
		String[] variables = new String[set.size()];
		int i = 0;
		for (Variable v : set) {
			variables[i] = v.toString();
			i++;
		}
		Arrays.sort(variables);
		int size = set.size();
		for (String s : variables) {
			Interval interval = intervalInfo.getIntervals().get(new Variable(s));
			res += "(" + s + ", ["+ interval.getLeft() + "," + interval.getRight() + "])";
			if (size > 1) {
				res += ", ";
				size--;
			}
		}
		res += "}";
		return res;
	}
	
	@Override
	public void postTransformCFG(CFG cfg) {
		for(CFGNode node:cfg.getAllNodes()){
			if(node.getAnalysisInfo() instanceof Bottom){
				for(CFGEdge edge:node.getInEdges()){
					edge.setLabel(new LabNop());
				}
				continue;
			}
			IntervalDomain info = (IntervalDomain) node.getAnalysisInfo();
			for(Variable v:GlobalConfig.variableSet){
				Interval i = info.getIntervals().get(v);
				if(i.getLeft().eq(i.getRight())){
					Constant c = new Constant(i.getLeft().getInt());
					for(CFGEdge e:node.getOutEdges()){
						e.getLabel().replaceVariable(v, c);
					}
				} 
				for(CFGEdge e : node.getOutEdges()) {
					if (e.getLabel() instanceof LabPos) {
						Interval absRes = ((LabPos) e.getLabel()).getCondition().abstractExpressionEvaluation(info);
						if (absRes.getLeft().eq(absRes.getRight()) 
								&& absRes.getLeft().eq(new IntervalBound(BigInteger.ONE, false, false))) {
							e.setLabel(new LabNop());
						}
					}
					if (e.getLabel() instanceof LabNeg) {
						Interval absRes = ((LabNeg) e.getLabel()).getCondition().abstractExpressionEvaluation(info);
						if (absRes.getLeft().eq(absRes.getRight()) 
								&& absRes.getLeft().eq(new IntervalBound(BigInteger.ZERO, false, false))) {
							e.setLabel(new LabNop());
						}
					}
				}
				
			}
		}
	}
	
	public AnalysisDomain edgeEffectNOP(CFGEdge edge) {
		if(edge.getFromNode().getAnalysisInfo() instanceof Bottom){
			return new Bottom();
		}
		IntervalDomain input = (IntervalDomain) edge.getFromNode().getAnalysisInfo();
		Map<Variable,Interval> output = new HashMap<Variable,Interval>(input.getIntervals());
		IntervalDomain info = new IntervalDomain(output);
		return info;
	}
	
	public AnalysisDomain edgeEffectPos(CFGEdge edge) {
		if(edge.getFromNode().getAnalysisInfo() instanceof Bottom){
			return new Bottom();
		}
		
		IntervalDomain input = (IntervalDomain) edge.getFromNode().getAnalysisInfo();
		Map<Variable,Interval> output;
		BinaryOp e = (BinaryOp) ((LabPos) edge.getLabel()).getCondition();
		Expression r = e.getLoperand();
		Interval res = e.getRoperand().abstractExpressionEvaluation(input);
		
		if(r instanceof Variable){
			// more information can be extracted from the type of comparison
			output = new HashMap<Variable,Interval>();
			Variable var_r = (Variable) r;
			Interval old_val = input.getIntervals().get(var_r);
			Interval new_val;
			
			IntervalBound left = new IntervalBound(null,true,false);
			IntervalBound right = new IntervalBound(null,false,true);
			IntervalBound o = new IntervalBound(BigInteger.ONE,false,false);
			switch(e.getOperator().getType()){
				case EQ:
					// TODO: is that correct?
					new_val = old_val.meet(res);
					break;
				case LE:
					new_val = old_val.meet(new Interval(left,res.getRight()));
					break;
				case GE:
					new_val = old_val.meet(new Interval(res.getLeft(),right));
					break;
				case GT:
					IntervalBound left_inc = res.getLeft().add(o);
					new_val = old_val.meet(new Interval(left_inc,right));
					break;
				case LT:
					IntervalBound right_dec = res.getRight().sub(o);
					new_val = old_val.meet(new Interval(left,right_dec));
					break;
				default:
					new_val = old_val;
					break;
			}
			// meet empty -> illegal meet, program point not reachable
			if (new_val == null) {
				return new Bottom();
			}
			
			for(Variable v:GlobalConfig.variableSet){
				if(v.equals(var_r)){
					output.put(var_r, new_val);
				} else {
					output.put(v, input.getIntervals().get(v));
				}
			}
			return new IntervalDomain(output);
		}
		
		// Cases like 5 > 8 might occur
		IntervalBound z = new IntervalBound(BigInteger.ZERO,false,false);
		Interval zero = new Interval(z,z);
		
		Interval condition = e.abstractExpressionEvaluation(input);
		
		if(condition.equals(zero)){
			// edge cannot be taken -> return Bottom
			return this.getBottom();
		} else {
			// edge can be taken -> keep AnalysisInformation from before
			output = new HashMap<Variable,Interval>(input.getIntervals());
			return new IntervalDomain(output);
		}
	}
	
	public AnalysisDomain edgeEffectNeg(CFGEdge edge) {
		if(edge.getFromNode().getAnalysisInfo() instanceof Bottom){
			return new Bottom();
		}
		
		IntervalDomain input = (IntervalDomain) edge.getFromNode().getAnalysisInfo();
		Map<Variable,Interval> output;
		BinaryOp e = (BinaryOp) ((LabNeg) edge.getLabel()).getCondition();
		Expression r = e.getLoperand();
		Interval res = e.getRoperand().abstractExpressionEvaluation(input);
		
		if(r instanceof Variable){
			// more information can be extracted from the type of comparison
			output = new HashMap<Variable,Interval>();
			Variable var_r = (Variable) r;
			Interval old_val = input.getIntervals().get(var_r);
			Interval new_val;
			
			IntervalBound left = new IntervalBound(null,true,false);
			IntervalBound right = new IntervalBound(null,false,true);
			IntervalBound o = new IntervalBound(BigInteger.ONE,false,false);
			switch(e.getOperator().getType()){
				case NE:
					// TODO: is that correct?
					new_val = old_val.meet(res);
					break;
				case GT:
					new_val = old_val.meet(new Interval(left,res.getRight()));
					break;
				case LT:
					new_val = old_val.meet(new Interval(res.getLeft(),right));
					break;
				case LE:
					IntervalBound left_inc = res.getLeft().add(o);
					new_val = old_val.meet(new Interval(left_inc,right));
					break;
				case GE:
					IntervalBound right_dec = res.getRight().sub(o);
					new_val = old_val.meet(new Interval(left,right_dec));
					break;
				default:
					new_val = old_val;
					break;
			}
			// illegal meet? -> bottom since not reachable
			if (new_val == null) {
				return new Bottom();
			}
			
			for(Variable v:GlobalConfig.variableSet){
				if(v.equals(var_r)){
					output.put(var_r, new_val);
				} else {
					output.put(v, input.getIntervals().get(v));
				}
			}
			return new IntervalDomain(output);
		}
		
		// Cases like 5 > 4
		IntervalBound o = new IntervalBound(BigInteger.ONE,false,false);
		Interval one = new Interval(o,o);
		
		Interval condition = e.abstractExpressionEvaluation(input);
		
		if(condition.equals(one)){
			// edge cannot be taken -> return Bottom
			return this.getBottom();
		} else {
			// edge can be taken -> keep AnalysisInformation from before
			output = new HashMap<Variable,Interval>(input.getIntervals());
			return new IntervalDomain(output);
		}
	}
	
	public AnalysisDomain edgeEffectAssign(CFGEdge edge) {
		if(edge.getFromNode().getAnalysisInfo() instanceof Bottom){
			return new Bottom();
		}
		IntervalDomain input = (IntervalDomain) edge.getFromNode().getAnalysisInfo();
		Map<Variable,Interval> in = input.getIntervals();
		Map<Variable,Interval> out = new HashMap<Variable,Interval>();
		Variable var = ((LabAssign) edge.getLabel()).getLeftSide();
		Interval res = ((LabAssign) edge.getLabel()).getRightSide().
				abstractExpressionEvaluation(input);
		
		for(Variable v:GlobalConfig.variableSet){
			if(v.equals(var)){
				out.put(v, res);
			} else {
				out.put(v, in.get(v));
			}
		}
		return new IntervalDomain(out);
	}
	
	public AnalysisDomain edgeEffectLoad(CFGEdge edge) {
		if(edge.getFromNode().getAnalysisInfo() instanceof Bottom){
			return new Bottom();
		}
		IntervalDomain input = (IntervalDomain) edge.getFromNode().getAnalysisInfo();
		Map<Variable,Interval> in = input.getIntervals();
		Map<Variable,Interval> out = new HashMap<Variable,Interval>();
		Variable var = ((LabLoad) edge.getLabel()).getLeftSide();
		
		for(Variable v:GlobalConfig.variableSet){
			if(v.equals(var)){
				IntervalBound left = new IntervalBound(null,true,false);
				IntervalBound right = new IntervalBound(null,false,true);
				out.put(v,new Interval(left,right));
			} else {
				out.put(v, in.get(v));
			}
		}
		return new IntervalDomain(out);
	}
	
	public AnalysisDomain edgeEffectStore(CFGEdge edge) {
		if(edge.getFromNode().getAnalysisInfo() instanceof Bottom){
			return new Bottom();
		}
		IntervalDomain input = (IntervalDomain) edge.getFromNode().getAnalysisInfo();
		Map<Variable,Interval> output = new HashMap<Variable,Interval>(input.getIntervals());
		IntervalDomain info = new IntervalDomain(output);
		return info;
	}

}
